0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 24 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇒, 0 ms)
↳8 QDP
↳9 QDPSizeChangeProof (⇔, 4 ms)
↳10 YES
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, ackermann_in_gga(s(M), N))
U2_GGA(M, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGA(M, Val1)
ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
ackermann_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)
From the DPs we obtained the following set of size-change graphs: